package projeto;

public interface Aresta {
	//@ public model instance nullable Vertice _vinicial;
	//@ public model instance nullable Vertice _vfinal;
	//@ public model instance double _esforco;
	//@ public model instance double _distancia;
	//@ public model instance double _angulo;
	//@ public model instance int _numero;
	//@ public model instance nullable String _nome;
	
    public /*@ pure @*/ Vertice getDestino();
    public /*@ pure @*/ double getEsforco();
    public /*@ pure @*/ double getAngulo(); 
    public /*@ pure @*/ double getDistancia();
    public /*@ pure @*/ Vertice getOrigem();
    public /*@ pure @*/ int getNumero();
    
	/*@ assignable _esforco;
	 @ ensures _esforco == iesforco;
	 @ */
	public void setEsforco(double iesforco);
	
	/*@ assignable _vfinal;
	  @ ensures _vfinal == destino;
	  @*/
	public void setDestino(Vertice destino); 
	
	/*@ assignable _vinicial;
	 @ ensures _vinicial == origem;
	 @*/
    public void setOrigem(Vertice origem);
    
    /*@ assignable _numero;
     @ ensures _numero == inumero;
     @*/
    public void setNumero(int inumero);
    
    /*@ assignable _angulo;
     @ ensures _angulo == iangulo;
     @*/
    public void setAngulo(double iangulo);
    
    /*@ assignable _distancia;
     @ ensures _distancia == idistancia;
     @*/
    public void setDistancia(double idistancia); 
    
}
